// Script to detect Ctrl+click
//    function mouseDown(e) {  
//        if (e.ctrlKey) {
//            alert("Ctrl click pressed.");
//        }
//        return true;
//    }
//    document.onmousedown = mouseDown;
//    document.captureEvents(Event.MOUSEDOWN);

function get_style_sheets() {
    var links = window.$("link[type='text/css']");
    var ret = [];
    for(var i = 0; i < links.length; i++) {
        ret[i] = links[i].href;
    }
    return ret;
}